\documentclass[orivec]{llncs}

\usepackage{headers}
\usepackage{macro}

%opening
\title{Activity networks with delays }
\author{Cinzia Di Giusto\inst{1} \and Jean-Luis Giavitto\inst{2}  \and Hanna Klaudel\inst{1} \and Antoine Spicher\inst{3} }
\institute{Université d'Evry - Val d'Essonne, Laboratoire IBISC, Evry, France
\and IRCAM - Music Representations Team, Paris \and LACL, Université Paris Est, Créteil}

\begin{document}


\maketitle

\begin{abstract}
We propose \andy, \emph{Activity Networks with DelaYs}, a discrete time framework devoted to qualitative modeling of time depending activities. 
Each activity involves entities that may represent objects (e.g., agents, bio-chemical species\dots or families of thereof) with a local state (a finite number of finitely valued attributes: location, concentrations, strength, expression levels\dots).

An \andy global state involves a set of entities at their respective local state. System dynamics corresponds to %both synchronous and asynchronous 
evolution of entities' state, described by a set of rules, called activities and involving entities that can play the role of activators, inhibitors or results in a static influence network.
Activities may have given durations and can take place only if all activators are available at a given state and all inhibitors are not present for the whole duration of the activity.
Depending on the type of activity, local states can be seen as levels that can be updated to achieve aging, degradation or other time dependent activities.

We define the model formally in terms of high level Petri nets and illustrate it with examples coming from various domains.
We show that the concept of time in \andy has a counterpart in timed automata, but the encoding is non trivial and above all exponential  thus limiting the use of this representation in practice.
Nevertheless, the theoretical foundation of \andy makes possible the analysis and the exploration of its behavior through model-checking techniques.
\end{abstract}
 
\section{Introduction}
	
TODO EXPLAIN BETTER HERE
	
In this paper, we define a modular modeling environment, 
called \andy for Activity Networks with DelaYs suitable 
for qualitative modeling of time-dependent systems.
Our goal is to model systems composed of various \emph{entities} that can be actors, agents or families of thereof. Entities are characterized by attributes, called \emph{levels}, such as rates of activation or expression degrees (e.g., low, medium, high), 
and involved in some (possibly time dependent) activities. 
A system state is given by a record of current entities levels together with a timing information necessary for enabling activities. 
Activities are rules involving three sets of entities:
 \emph{activators}, %, which must be present and 
 \emph{inhibitors} and  \emph{results}. 
%which must be absent during the whole time interval the activity takes place.
Depending of their kind, \emph{obligatory} or \emph{potential}, 
activities must or may be activated producing eventually a change of entities levels in the results set.
Moreover, some entities are subject to a \emph{decay} process or aging that models the action of a non-specified environment and as time passes by it decreases theirs levels.
Thus, a system evolution shows how the entities levels change along time.

%\paragraph{\bf Introductory example.} 
\begin{example}[Mobile phone battery] \label{ex:battery}
Take for instance the example of a battery of a mobile phone. 
We identify its charge as an entity having a few levels. 
For the sake of the example, say $5$ levels, from $0$ the minimal level of charge to $4$ meaning full charge. 
The evolution of the model shows how the values of charge levels change along time complying to the following: 
\begin{enumerate}
	\item \label{it:decay} The level of mobile phone charge diminishes continuously, even when it is not used for making a phone call; it diminishes slowly when it is fully charged and faster when it is partly discharged;
	\item \label{it:plug} The mobile phone may be plugged to start charging, which takes some time to reach full charge;
	\item \label{it:call} If charged enough, the mobile phone may be used to make phone calls but its charge diminishes; 
	\item \label{it:GPS} Similarly, GPS navigation needs more charge and consumes battery faster.
\end{enumerate}
Item (1) corresponds to the decay process, while the other three items represent activity rules. Item (2) is modeled with an auxiliary entity representing the plug (which may be on or off). The action of plugging the mobile phone is a potential activity. If plugged the battery starts charging which is represented by an obligatory  activity augmenting its charge level. Item (3) and (4) are implemented similarly, using two more entities one for the call and the other for GPS navigation. \hfill $\diamond$
\end{example}
TODO: ADD SCENARIO IN WORDS


%%%%%%%%
%\paragraph{\bf Our contribution.}
TODO: FIX CONTRIBUTION HERE

%Entities are available at a given discrete   
%level, and there is a finite number of levels for each entity.  
%Time plays a role in the evolution of entities themselves and in the duration of activities. 
%More precisely, entities may have an associated aging function $\delta$, meaning that their  
%level diminishes with time.
%As mentioned above, this accounts for the presence of a non-specified environment that consumes and degrades entities, 
%thus allowing to abstract away from activities that may be neglected in the specified context.
%
%An activity $\alpha$ of duration $\Delta_\alpha$ 
%can take place only if each activator in $A_\alpha$ stays at least at a given level and each involved 
%inhibitor in $I_\alpha$ is at most at a given level during the whole activity time. 
%As a result, the level of entities of the activity results in $R_\alpha$ can be increased, decreased or simply maintained.

We give the definition of \andy networks using high-level Petri nets.
The obtained model is compact and provides an intelligible graphical representation of the described activities. Moreover, the network is easily scalable: the size of the network grows linearly with the number of added entities and activities. 
Then, we provide different examples of modeling with \andy, in various contexts.


TO BE DETAILED
Finally, in order to asses the time concept used in \andy, and its expressive power, we provide its encoding in a suitable class of timed automata. 


As main results, we show that: %HK devrait etre reredige mieux que ca :-(
\begin{itemize}
	\item \andy is suitable for qualitative modeling of time dependent and entities based systems; 
	\item \andy's state space is finite enabling automatic analysis using model-checking techniques;
	\item \andy's representation is efficient compared to the equivalent representation in terms of timed automata.
\end{itemize}

{\bf Organization of the paper.} 
The paper is organized as follows:  
 Section \ref{sec:reaction} introduces the principles behind \andy networks. Section \ref{sec:petri} presents their definition in terms of high-level Petri nets.   
Next, Section \ref{sec:example} shows some examples of modeling via \andy networks.
Section \ref{sec:timedauto} presents the translation of \andy networks into a suitable
class of timed automata. 
Finally, Section \ref{sec:concl} discusses related works and concludes with some considerations on future work. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Syntax and intuitive semantics} \label{sec:reaction}
In this section we describe the syntax and semantics  of \emph{Activity Networks with Delays} (\andy). 
As mentioned in the introduction an \andy network is composed of a set of entities \entities governed by a set of activities.
 
Entities $\gamma$ in  \entities represent the actors of the modeled system. They could be concrete objects or more abstract concepts such as rates or states of an object (e.g. the level of charge of a mobile phone battery). 
Entities have a finite number of levels $\setlev$ from 0 to $\setlev-1$, in general they represent ordered expression degrees (e.g. low, medium, high) and they  refer to a change in their capability of action. 
 Each  $\gamma$ is initialized at a certain  level $\level{\gamma}$ and each level is associated to a decay duration which is either $\omega$ (unbounded) or a finite natural number (thus allowing different durations for different levels):  
\[ 
\life_\gamma:[0..\setlev_\gamma-1] \to \nat^+ \cup \{\omega \}.
\]
For each entity $\gamma$, we set  $\life_{\gamma}(0) = \omega$.  
 $\life_\gamma(i) \neq \omega$ indicates that the presence of the entity at that level is ephemeral, in other words by effect of an unspecified environment, it decays or ages gradually (e.g. decreasing the level) as time passes by. 
On the contrary, if $\life_\gamma(i) = \omega$, entity levels are permanent and  they  can be modified only by activities.
 
\begin{example}[Mobile phone battery - entities]


We model here Example \ref{ex:battery} given in the introduction. The set of entity involved with corresponding levels and associated decay is:
 $$ \begin{array}{llll}
     \text{Battery}\quad  & B &\setlev_{B}=\{5\} & \life_{B}(i)=2 \text{ for }  0<i \leq 3,  \quad \life_{B}(4)=3\\
      \text{Plug} &P \ &\setlev_{P}=\{2\} &  \\
     \text{Call} & C &\setlev_{C}=\{2\} \ &  \\
			\text{GPS} &G &\setlev_{G}=\{2\} \ &  
    \end{array}
$$
where unspecified decays are all set to $\omega$.
Decay durations are used to model Item (\ref{it:decay}) in page \pageref{ex:battery}. Notice that in the modeling of entity $B$ they are not uniform to denote different speeds in the consumption of the charge (\ie for the full charge level 4 decay takes 3 units of time while for the others it is 2).
All other entities have only two levels, roughly speaking on/off, encoded as 0=off and 1=on.
Environment has no role in the evolution of the levels of these entities that are therefore set to unbounded duration $\omega$.  
\hfill $\diamond$
\end{example}


The evolution of entities is governed by a set of \emph{activities} of the form: 
\begin{equation}\label{eq:reaction}
 \activ{A}{I}{\dur{}}{R}
\end{equation}
 where $\dur{} \in \nat$ is the activity duration,  $A$ (activators), 
$I$ (inhibitors) are sets of pairs $(\gamma, \level{\gamma})$ 
and $R$ (results) is a non empty set of pairs $(\gamma, v)$, 
where $\gamma\in \entities$,  $\level{\gamma} \in [0..\setlev_\gamma-1]$ 
and $v  \in \mathbb{Z}$. Duration characterizes the time required for yielding change of  levels of results, $\dur{} =0 $ denotes an instantaneous  activity.
 Entities can appear at most once in each set $A$, $I$ and $R$. They can be present in both $A$ and $I$ but they must occur with different levels. 
Activities can be of two types:
\begin{enumerate}
 \item \emph{Obligatory}, denoted $\beta$ in a set $\Syn$: if enabled at some date, they \emph{must} occur. All enabled obligatory activities occur simultaneously.  
 \item \emph{Potential}, denoted $\alpha$ in a set $\Reac$: if enabled at some date, they \emph{may} occur and the result  depends on the order they are performed.
\end{enumerate}

\begin{example}[Mobile phone battery - activities]
The description of actions in Items (2-4) in page \pageref{ex:battery} gives rise to the following sets of activities. 
Item (\ref{it:plug}) may be described by two potential instantaneous activities $\alpha_1, \alpha_2$, that model plugging and unplugging respectively, and an obligatory activity $\beta_1$ with duration 1 that models the recharging process.  

$$
\begin{array}{ll  ll}
\alpha_1: & \activ{(P,0)}{(P,1)}{0}{(P,+1)} \qquad &  \beta_1: & \activ{(P,1)}{\emptyset}{1}{(B,+1)} \\
\alpha_2: & \activ{(P,1)}{\emptyset}{0}{(P,-1)}
\end{array}
$$

Similarly, Item (\ref{it:call}) may be depicted by two potential instantaneous activities $\alpha_3, \alpha_4$ modeling the start and the end of a call phone  respectively, and an obligatory activity $\beta_2$ with duration 3 defining the discharging process due to the call.\looseness=-1 

$$
\begin{array}{ll ll}
\alpha_3: & \activ{(C,0)}{(C,1)}{0}{(C,+1)} \qquad & \beta_2: & \activ{(C,1)}{\emptyset}{3}{(B,-1)} \\
\alpha_4: & \activ{(C,1)}{\emptyset}{0}{(C,-1)} 
\end{array}
$$


Finally Item (\ref{it:GPS}) may again be described by two potential instantaneous activities $\alpha_5, \alpha_6$ that model activation and deactivation of GPS navigation respectively, and an obligatory activity $\beta_3$ with duration 3 that models the discharging process due to the GPS usage. Notice that in this case, even if duration is the same, the battery is consumed faster than a simple phone call (indicated by $(B, -2)$ instead of $(B, -1)$ ).   

$$
\begin{array}{ll ll}
\alpha_5: & \activ{(G,0)}{(G,1)}{0}{(G,+1)}\qquad &  \beta_3: & \activ{(G,1)}{\emptyset}{3}{(B,-2)} \\
\alpha_6: & \activ{(G,1)}{\emptyset}{0}{(G,-1)} 
\end{array}
$$
\hfill$\diamond$
\end{example}


 
Thus, an \andy network is a triple $(\entities, \Syn, \Reac)$ where $\entities$ is the set of entities, $\Syn$ is the set of obligatory activities and $\Reac$ is the set of potential ones.
The dynamics of \andy is formalized using  high-level Petri nets. 
Before specializing these nets, we describe the intended behavior of \andy. 
We assume that time is discrete. Time is used to decide whether an entity has to decay or to verify whether an activity is enabled or not.

 
We represent the state of an entity $\gamma$ as a tuple 
$\tuple{\bool_\gamma, \refr_\gamma, \birth_\gamma}$ where 
$\bool_\gamma$ is an integer value storing  the current   
level from zero to $\setlev_\gamma -1$; 
$\refr_\gamma$ is the amount of time spent in the current    
level since the last update: $0 \leq \refr \leq \life_\gamma(\bool_\gamma)$; 
and $\birth_\gamma$ is a tuple with $\setlev_\gamma$ 
fields (one for each  level) each $\birth[j]$ 
containing the length  of time interval from 0 to a constant $D$ where $D = \max\{\dur{\rho} \mid \rho \in \Syn \cup \Reac\}$. 

The system is initialized by setting the  level of all entities: 
\ie  each entity $\gamma$ is set to $\tuple{\level{\gamma}, 0, 0^{\setlev_\gamma} }$ 
where $\level{\gamma}$ is the given initial level and $0^{\setlev_\gamma}$ 
denotes vector $\birth_\gamma$ uniformly initialized with zero.

\begin{example}[Mobile phone battery - initial state]
The initial levels for the battery example are $(B, 4), (P, 0), (C, 0), (G,0)$.
Thus, the initial state for each entity is:
$$
 B=\tuple{4, 0, [0,0,0,0,0]}
 \quad P=\tuple{0, 0, [0,0]}
 \quad C=\tuple{0, 0, [0,0]}
 \quad G=\tuple{0, 0, [0,0]}\quad  \diamond
$$
\end{example}


\begin{newnotation}
We denote by $\birth\sub{x}{[l \dots l + n ]}$
the systematic update of values in $\birth[l] \dots \birth[l+n]$ to $x$,
and by $\inc{D}{\birth}$ the increment by one of all values  in $\birth$: \ie
$\forall k \in [0.. \setlev_\gamma-1]$, $\birth[k] = \min(\birth[k]+1, D)$
\end{newnotation}


An activity $\rho \in \Syn \cup \Reac$ may happen if  all  entities $\gamma_a$ of activators $(\gamma_a, \level{a})$ are available 
at least at  level $\level{a}$ and all entities $\gamma_i$ of inhibitors $(\gamma_i, \level{i})$ are expressed at a level 
strictly inferior to $\level{i}$ for the whole response time period $\dur{\rho}$. 
The triggering of an activity has as effect an update of the fields of its results. Activators and inhibitors are left unchanged unless explicitly indicated in results.%, thus activities do not compete over entities. 
More precisely, assume a result $r$ at level $\lev_r$  and $n\in \nat$, thus $\tuple{\lev_r, \refr_r, \birth_r}$ is updated to:
\begin{description}
 \item[Increase $+n$:]  
   $\tuple{\lev_r + n, 0, \birth_r\sub{0}{[\lev_r + 1\dots \lev_r + n]}}$.
Notice that  $\lev_r$ becomes $\lev_r +n$, $\refr_r$ is reset to 0 starting a new time interval for level $\lev_r +n$ and 
$\birth_r$ is updated to record the change to the new level 
for all levels from $\lev_r + 1$ to $\lev_r + n$.
 
 \item[Maintenance $0$:]  $\tuple{\lev_r, 0, \birth_r}$: \ie the current level is recharged resetting $\refr_r$ to 0.

  \item[Decrease $-n$:]  
	    $\tuple{\lev_r - n, 0, \birth_r\sub{0}{[\lev_r-n+1 \dots \lev_r] }}$. This case is symmetric to the increase one.
\end{description}
Once performed, the next execution of the same activity is possible after at least $\dur{\rho}$ time units.

\andy networks can evolve in two ways: 
\begin{enumerate}[{Case} 1.]


\item  \label{item:reaction} {\bf Potential activity: }
At each time unit, enabled activities may take place in an interleaved way and they are instantaneous (\ie time does not pass by).


\item \label{item:clock} {\bf Clock:} 
This is the time transition, it regards all entities. In this step, we register the progression of time with related decay of concerned entities  and all enabled obligatory activities are performed simultaneously. 
\begin{description}
 \item [Time: ] All intervals in the entities are incremented by one: we pass from  
$\tuple{\lev, \refr, \birth}$ to $\tuple{\lev, \refr+1, \inc{D}{\birth}}$.
We assume that the value $\refr$ remains unchanged for levels of unbounded duration, and once a value in $\birth$ has reached $D$ it is useless to increment it, as for all values greater than $D$ (the maximal duration of activities), the guard of all activities involving the entity is satisfied.      

 \item [Decay: ]An entity may stay at level $\lev$ for $\life(\lev)$ time units (\ie $\refr \leq \life(\lev)$).  
Decay happens as soon as the interval $\life(\lev)$ is elapsed and 
is obtained by decreasing the level by one, till reaching level zero.  
More formally, we pass from  
$\tuple{\lev, \refr, \birth}$ to $\tuple{\lev - 1, 0, \inc{D}{\birth}\sub{0}{\lev}}$.

\item [Obligatory activity: ] Enabled obligatory activities  happen simultaneously\footnote{Notice that as activators and inhibitors are not consumed, there are no conflicts and so there is a unique way (per time unit) to execute all enabled obligatory activities}  and the results levels are summed up.  
\end{description}
\end{enumerate}



As a direct consequence of the description of the evolutions of \andy,  for each entity ${\gamma}$ that is currently at level $\lev_{\gamma}$,
the tuple $\birth_{\gamma}$ contains, for each level, an interval of time interpreted as follows: 
$$
\birth_{\gamma}[i] = 
\begin{cases}
\begin{minipage}{7cm}
 the interval of time indicating when $\gamma$ changed its level to  $i$
\end{minipage}
 &  \text{for }  0 \leq i \leq \lev_{\gamma}\\
\\
\begin{minipage}{7cm}
  the interval of time indicating when $\gamma$ was at level $i$ or $0$ if $\gamma$ has not yet reached $i$.
\end{minipage} 
& \text{for } \lev_{\gamma} < i \leq \setlev_{\gamma}-1              
\end{cases}
$$

\begin{example}[Mobile phone battery - Execution scenario]

As mentioned before,  the initial state is
$$
\begin{array}{c|c|c|c}
B &P&C&G\\
\quad \tuple{4, 0, [0,0,0,0,0]} \quad 
 & \quad \tuple{0, 0, [0,0]} \quad 
 &\quad  \tuple{0, 0, [0,0]}\quad 
 &\quad  \tuple{0, 0, [0,0]}\quad 
\end{array}
$$
we activate the GPS ($\alpha_5: \activ{(G,0)}{(G,1)}{0}{(G,+1)}$)
$$
\begin{array}{c|c|c|c}
\quad \tuple{4, 0, [0,0,0,0,0]}\quad
 &\quad \tuple{0, 0, [0,0]}\quad
&\quad \tuple{0, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad
\end{array}
$$
start a phone call ($\alpha_3: \activ{(C,0)}{(C,1)}{0}{(C,+1)}$)
$$
\begin{array}{c|c|c|c}
\quad \tuple{4, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [0,0]} \quad
 &\quad \tuple{1, 0, [0,0]}\quad
 &\quad \tuple{1, 0, [0,0]}\quad 
\end{array}
$$
3 time units pass by (no decay or obligatory activity involved)
$$
\begin{array}{c|c|c|c}
\quad
 \tuple{4, 3, [3,3,3,3,3]} \quad
& \quad \tuple{0, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]}\quad
\end{array}
$$
1 time unit pass by, battery decays, and enabled obligatory activities\\ $\beta_2: \activ{(C,1)}{\emptyset}{3}{(B,-1)}, \beta_3: \activ{(G,1)}{\emptyset}{3}{(B,-2)}$ are performed
$$
\begin{array}{c|c|c|c}
\quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{0, 0, [3,3]}\quad
& \quad \tuple{1, 0, [3,3]}\quad
& \quad \tuple{1, 3, [3,3]}\quad
\end{array}
$$
we plug the phone ($\alpha_1:  \activ{(P,0)}{(P,1)}{0}{(P,+1)}$)
$$
\begin{array}{c|c|c|c}
\quad
 \tuple{0, 0, [0,0,0,0,0]} \quad
& \quad \tuple{1, 0, [3,0]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
& \quad \tuple{1, 0, [3,3]} \quad
\end{array}
$$
1 time unit passes by with no decays and enabled obligatory activity\\
$\beta_1:\activ{(P,1)}{\emptyset}{1}{(B,+1)}$ is executed
$$
\begin{array}{c|c|c|c}
\quad
 \tuple{1, 0, [1,0,1,1,1]} \quad
 &\quad \tuple{1, 0, [3,1]} \quad
 &\quad \tuple{1, 0, [3,3]} \quad
 &\quad \tuple{1, 0, [3,3]} \quad
\end{array}
$$
An implementation of this example in Petri nets is given in Appendix \ref{app:mobile}.
\hfill $\diamond$
\end{example}




It is also worth observing that if an entity is continuously sustained  by some activities then it remains available in the system at a certain  level for a period that could be longer than the corresponding decay time. This is witnessed by the fact that the values of fields $\birth[\lev]$ and $\refr$ can be different: the first representing the  availability at level $\lev$ and the second the interval since last update. 


Finally, we comment on some specific design choices concerning activities:
\begin{itemize}
 \item the set of activators and inhibitors $A \cup I $ is allowed to be empty. This accounts for modeling an environment that is continuously sustaining the production of an entity. In this case the response time is always set to 0 as it is  not significant;  
 \item an entity can appear in the same activity simultaneously as an activator and an inhibitor. In such a case, we require them to occur with  different levels: 
$$(\{({\gamma},\level{})\} \cup A, \{({\gamma}, \level{}')\} \cup I , R )$$
where $\level{}< \level{}'$. This means that the activity  can take place only if the level $\lev_{\gamma}$ of ${\gamma}$ belongs to the interval $\level{} \leq \lev_{\gamma} < \level{}'$. In particular, if ${\gamma}$ has to be present  in a activity exactly at level $\level{}$, ${\gamma}$ should appear as an activator at level $\level{}$ %(that has to be present at least at level $\level{}$) 
and as inhibitor at level $\level{}'=\level{}+1$;% (that has to be at least at level strictly less than $\level{}+1$).
 \item  entities can appear only once in the set of results $R$. This implies that a result cannot be increased or decreased in the same activity.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Petri net model}\label{sec:petri} 


We recall here the general notations together with some elements of  the semantics of high-level Petri nets \cite{DBLP:series/eatcs/Jensen92}.

\begin{definition}[high-level Petri nets]\label{def:PTS}
A \emph{high-level Petri net} $N$ is a tuple $(P, T, F, L, M_0)$ where:
\begin{itemize}
 \item $P$ is the set of places, $T$ is the set of transitions, with $P \cap T = \emptyset$;

 \item $F \subseteq (P \times T) \cup (T \times P)$ is the set of arcs; 
 \item $L$ is the labeling  of $P \cup T\cup F$%places $P$, transitions $T$ and arcs $F$   to  a set of labels 
defined as follows:
\renewcommand{\labelitemii}{$-$} 
\begin{itemize}
 \item $\forall p \in P$, $L(p) $ is a set of values;% the type of $p$;%, \ie a (possibly infinite) set or Cartesian product of sets of integer values;
 \item $\forall t \in T$, $L(t)$ is a  computable boolean expression (a guard);%  with variables and integer values; 
 \item and $\forall f\in F$, $L(f)$  is a  tuple of variables or values.% compatible with the adjacent place.  
\end{itemize}
 \item $M_0$ is the initial marking putting a multiset of tokens in $L(p)$ in each   $p \in P$.\looseness=-1
\end{itemize} 
\end{definition}

Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction  for each pair place/transition   is allowed and only one token can flow through. 
We denote the set of input places of a transition $t$ by 
$\pre{t} =\{p\in P \mid (p,t) \in F\}$. 
The behavior of high-level Petri nets is defined as usual: markings are functions from places in 
$P$ to multisets of tokens $L(p)$ and  a transition $t \in T$ is \emph{enabled} at  
marking $M$, if there exists an evaluation $\sigma$ of all variables in the labeling 
of $t$ and of its adjacent  input and  output arcs such that: 
\[
L_{\sigma}(t) = \mathsf{true}  \qquad \text{ and } \qquad \forall p \in \pre{t},   
L_{\sigma}((p,t)) \in M(p).
\]
then, the firing of $t$ produces the marking $M'$,  
denoted $\firing{M}{t}{\sigma}{M'}$:  
\[
\forall p \in P, M'(p) = M(p) - L_{\sigma}((p,t)) + L_{\sigma}((t,p)). 
\]
with $L_{\sigma}(f) = 0$ if $f\notin F$, $-$ and $+$ are  multiset  operators for removal and adding of one element, respectively.

As usual, in figures, places are represented as rounds, transitions as squares, 
and arcs as directed arrows.
By convention, primed version of variables (e.g. $x'$) are used to annotate 
output arcs of transitions, their evaluation is  
possibly computed using unprimed 
variables (e.g. $x$) appearing on input arcs. 
With an abuse of notation, singleton markings are denoted without brackets, 
the same is used in  arc annotations. An example of firing is shown in  
Appendix \ref{app:exfiring}. 
We say that a marking $M$ is \emph{reachable} from the initial marking 
$M_0$ if there exists a firing sequence $(t_1, \sigma_1), \dots, (t_n, \sigma_n)$ such that 
 $\firing{M_0}{t_1}{\sigma_1}{M_1} \dots \firing{M_{n-1}}{t_n}{\sigma_n}{M}$.




\paragraph{\bf Petri net modeling of \andy.}

Each entity $\gamma \in \entities$ is modeled by a single place $p_{\gamma} $ whose type   $ L(p_{\gamma})$ is the set of  tuples of the form  $\tuple{\lev_{\gamma}, \refr_{\gamma}, \birth_{\gamma}}$, where $\lev_{\gamma} \in [0..\setlev_{\gamma}-1]$, $\refr_{\gamma} \in [0..\setlev_{\gamma}-1]$, $\birth_{\gamma} \in [0..D]^{\setlev_s}$. 
In order to cope with time aspects present in \andy, we have a special transition $t_c$ ((Figure \ref{fig:clock}) that represent the time progression. It is responsible of incrementing the length of time intervals in entities,  takes care of the decay and performs all enabled obligatory activities as described by Case \ref{item:clock} above.  
Finally, every potential activity $\alpha$ is modeled with  a transition $t_{\alpha}$ (Figure \ref{fig:reaction}) with a special place $p_{\alpha}$ that  ensures that the same activity is not executed more than once every $\dur{\alpha}$ time units.


\begin{figure}[t]
\centering
\subfigure[Clock transition. \label{fig:clock}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

  \node [place, label = right: $p_{\alpha}$, label = above: $\vdots$,label = below: $\vdots$] at (3.5,0) (Pc){};
  \node [place, label=left:$p_{\gamma}$,label = above: $\vdots$,label = below: $\vdots$]at (0,0)  (R){};

  \node [transition] (tC) at (2,0) {$t_{c}$}
   edge [pre,bend left]    node[above] {$w_{\alpha}$}    (Pc)
   edge [post,bend right]   node[below]{$w'_{\alpha}$}    (Pc)
   edge [pre,bend right]    node[above] {${\scriptstyle \tuple{\bool_{\gamma},\refr_{\gamma},\birth_{\gamma}}}$}    (R)
   edge [post,bend left]    node[auto] {${\scriptstyle \tuple{\bool_{\gamma}',\refr_{\gamma}',\birth_{\gamma}'}}$}    (R);
  
\end{tikzpicture}
} \quad
\subfigure[Transition for $\alpha\in\Reac$. \label{fig:reaction}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

 \node [place, label = right: $p_r$,label = left: $\cdots$] at (0,-1.5) (P){};
 %\node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = below: $p_a$,label = above: $\vdots$] at (-2,0) (R){};
 \node [place, label = below: $p_i$,label = above: $\vdots$] at (2,0) (I){};
 \node [place, label = right: $p_{\alpha}$,label = left: $\cdots$] at (0,1.5) (qw){};
 
 \node [transition] at (0,0) (tr) {$t_{\alpha}$}
  % edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\gamma},\refr_{\gamma},\birth_{\gamma}}}$}   (R)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\gamma},\refr_{\gamma},\birth_{\gamma}}}$}     (I)
   edge [pre, bend right]    node[left] {${\scriptstyle \tuple{\bool_{\gamma},\refr_{\gamma},\birth_{\gamma}}}$}   (P)
   edge [post, bend left]   node[right] {${\scriptstyle \tuple{\lev'_r,\refr'_r,\birth_r'}}$}     (P)
   edge [pre, bend left]    node[left] {$w_{\alpha}$}   (qw)
   edge [post, bend right]   node[right] {$w'_{\alpha}$}     (qw);
   
  
\end{tikzpicture}
}
\caption{Scheme of Petri net modeling of \andy.}
\end{figure}



\begin{definition}[\rsd network]\label{def:rs}
 Given an  \andy network $(\entities, \Syn, \Reac)$ with initial 
state $(\gamma, \level{\gamma})$ for each $\gamma \in \entities$, 
%Let $D = \max\{\dur{\alpha} \mid \alpha \in \Syn \cup \Reac\}$. 
the high-level Petri net representation is defined as 
tuple $(P, T, F, L, M_0)$ where  $\lev$, $\lev'$, $\refr$, $\refr'$, $\birth$, 
$\birth'$, $w$, $w'$ are variables and:
\begin{itemize} 
 \item $P = \{p_\gamma \mid  \gamma\in{\entities}\} \cup \{p_{\rho} \mid  \rho \in \Syn \cup \Reac \}; $
 \item $T= \{t_c \} \cup \{t_{\alpha} \mid \alpha \in \Reac \}$;

 \item $F= \{(p,t_c),(t_c, p) \mid p \in P \} \quad  \cup$ \\
 \hspace*{0.63cm} $ \{ (p_\gamma,t_{\alpha}),(t_{\alpha}, p_\gamma), (p_{\alpha},t_{\alpha}),
		(t_{\alpha}, p_{\alpha}) \mid \alpha \in \Reac, 
		\gamma \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}$

 \item Labels for places in $P$: 
\[
\begin{array}{c}
  L(p_{\rho})  = [0..D]  \text{ for each } \rho \in \Syn \cup \Reac  \\
L(p_\gamma) = [0..\setlev_\gamma-1] \times [0..d] \times  [0..D]^{\setlev_\gamma}  
\text{ for each } \gamma\in\entities 
\end{array}
\]
with $d = \max(\life_{\gamma}(i)\mid i \in [0..\setlev_\gamma-1])$
\item Labels for arcs in $F$:
\[
\begin{array}{llr}
 L((p_{\rho}, t_c)) = w_{\rho} & L((t_c, p_{\rho} )) = w'_{\rho}\\
    L((p_\gamma, t_c)) = \tuple{\bool_\gamma, \refr_\gamma, \birth_\gamma} 
		& L((t_c, p_\gamma)) = \tuple{\bool_\gamma', \refr_\gamma', \birth_\gamma'} 
		& \text{ for each } \gamma\in\entities
\end{array}
\]
For each potential activity $\alpha\in\Reac$ and $\gamma \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha}$:
\[
\begin{array}{llr}
      L((p_\gamma, t_{\alpha})) = \tuple{\bool_\gamma, \refr_\gamma, \birth_\gamma} \quad 
		& L((t_{\alpha}, p_\gamma)) = \begin{cases}
                           \tuple{\bool_\gamma, \refr_\gamma, \birth_\gamma} & \text{if } \gamma\notin R_{\alpha}\\
                           \tuple{\bool_\gamma', \refr_\gamma', \birth_\gamma'} & \text{otherwise}
                          \end{cases}\\

     L((p_{\alpha}, t_{\alpha})) = w_{\alpha} & L((t_{\alpha}, p_{\alpha} )) = w'_{\alpha}
\end{array}
\]



\item Labels for transitions in $T$:
 \[
 L(t_c) = \mathit{Calc}
 \]
where $\mathit{Calc}$ is the  algorithm in Figure \ref{fig:calc} that computes the updates 
to all places as a consequence of decay and/or obligatory activities. It always returns $\true$.
\begin{figure}[t]
\[
\begin{array}{l}
\mathit{Calc}\\
\text{for each } \rho \in \Syn \cup \Reac \text{ do } w_{\rho}'=\max(w_{\rho}+1,D)\\
%\text{endfor}\\

\text{for each } \gamma\in\entities \text{ do}\\
\qquad \lev_\gamma'=\lev_\gamma 
\qquad \refr_\gamma'=\refr_\gamma
\qquad \birth_\gamma'=\inc{D}{\birth_\gamma}\\
\qquad \text{if }  \life(\lev_\gamma) \neq \omega \text{ then } \quad \refr_\gamma'= \refr_\gamma + 1\\
\qquad \text{if } \refr_\gamma > \life(\lev_\gamma) \text{ then } \quad \lev_\gamma'= \max(0, \lev_\gamma -1)  
\quad  \refr_\gamma'= 0 \\
%\text{endfor}\\

\text{for each } \beta \in \Syn \text{ do}\\
\qquad \text{if } \bigwedge_{(a, \level{a}) \in A_{\beta}}(\lev_a \geq \level{a} \wedge  \birth[\level{a}] \geq \dur{\beta} )  \quad \wedge\\
\qquad \quad \bigwedge_{(i, \level{i}) \in I_{\beta}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\beta} )  \quad \wedge 
 \quad (w_{\beta} \geq \dur{\beta}  )
 \text{ then }\\
 \qquad \qquad w'_{\beta} = 0\\
 \qquad \qquad \text{for each } (r,v)\in R_{\beta} \text{ do} \\
 \qquad \qquad \qquad \lev_r'= \max(0, \min(\lev_r' +v, \setlev_r-1 )\\
\qquad  \qquad \qquad \refr_r'= 0\\
%\qquad \qquad \text{endfor} \\
%\qquad \text{endif}\\

\text{for each } \gamma \in \entities \text{ do}\\ %Est-ce bien ça ? no c'etait un typo
\qquad \text{case } \lev_\gamma' - \lev_\gamma \text{ of}\\
\qquad \qquad [\lev_\gamma' - \lev_\gamma<0]:  \birth_\gamma'=\birth'_\gamma\sub{0}{[\lev_\gamma'+1\dots \lev_\gamma]}\\
\qquad \qquad [\lev_\gamma' - \lev_\gamma>0]:  \birth_\gamma'=\birth_\gamma'\sub{0}{[ \lev_\gamma+1 \dots \lev_\gamma']}\\
%\qquad \text{endcase}\\


%\text{endfor}\\
\text{return } \true
\end{array}
\]
\caption{$\mathit{Calc}$ algorithm} \label{fig:calc}
\end{figure}

 
 
 
For each activity $\alpha\in\Reac$:
\[
\begin{array}{lcl}
L(t_{\alpha}) \! &=&  w_{\alpha} \geq \dur{\alpha}  \wedge  w'_{\alpha} = 0 \quad \wedge \\
&& \bigwedge_{(a, \level{a}) \in A_{\alpha}}(\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{\alpha} )  \quad \wedge\\
&&  \bigwedge_{(i, \level{i}) \in I_{\alpha}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\alpha} )  \quad  \wedge \\


&& \bigwedge_{(r,+n) \in R_{\alpha}} C_{r+} \wedge \bigwedge_{(r,0) \in E_{\alpha}}C_{r0} \wedge  \bigwedge_{(r,-n) \in R_{\alpha}}C_{r-},\\  
\end{array}
\]
with
\[
\begin{array}{lcl}


C_{r+} &:&  \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 .. \min(\lev_r +n, \setlev_r-1 ]}} \\
C_{r0} &:&  \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} \\

C_{r-} &:&  \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n).. \lev_r]}}.
\end{array}
\]

 

\item For each $p\in P$, $\gamma\in \entities$ and $\alpha\in \Reac$, the initial marking $M_0$ is:
\[
M_0(p) =
\begin{cases}
 0 & \text{if } p = p_{\rho}, \\
 \tuple{\level{s},0,0^{\setlev_\gamma}}& \text{if } p = p_\gamma.
\end{cases}
\]
\end{itemize}
\end{definition}


We now comment on the transitions guards. With an abuse of notation, in the following, we refer to evaluated variables without effectively mentioning the evaluation $\sigma$: \ie we say that the current value of a place $p_{\alpha}$ is $w$ instead of $\sigma(w)$.
Input and output arcs between the same place and transition with the same label (read arcs) are denoted in figures with a double-pointed arrow with a single label.
 We detail the conditions and the results of firing of $t_{\alpha}$ corresponding to a potential activity $\alpha= \activ{A}{I}{\dur{}}{R}$. We have:
\begin{itemize}
 \item each activator $a \in A$ has to be present at least at  level $\level{a}$ for at least $\dur{\alpha}$ time units, this is expressed by  guard $\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{\alpha} $; 
 \item each inhibitor $i\in I$ has not to exceed  level $\level{i}$ for at least $\dur{\alpha}$ time units,  this is guaranteed by guard 
$(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur(\rho) )$;
\item each result is updated according to conditions $C_{r+}$ (increase), $C_{r0}$ (maintenance), $C_{r-}$ (decrease);
\item place $p_{\alpha}$ retains whether the activity can been performed $w\geq\dur{\alpha}$.

%
%if a result $r \in R $ has to be increased maintained or decreased then the corresponding place $p_r$ is updated to:
%\begin{description}
 %\item [increase:] $\tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 .. \min(\lev_r +n, \setlev_r-1 ]}}$
 %\item [maintenance:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} $
 %\item [decrease:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n).. \lev_r]}}$. 
%\end{description}
\end{itemize}
Firing of transition $t_c$ is always enabled and all connected places are modified according to algorithm $\mathit{Calc}$: which increments the length of time interval in $p_{\rho}$ ($w'_{\rho} = w_{\rho}+1$) for all $\rho \in \Syn \cup \Reac$ unless an obligatory activities $\beta$ is performed in which case the corresponding $w_{\beta}$ is set to 0 and updates the level of all entities dependently if they are involved in an obligatory activity or decay.


ADD THEOREM/DISCUSSION ON THE FINITENESS OF STATE SPACE

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Examples}\label{sec:example}
In this section we provide some modeling examples using \andy.

REPRESSILATOR EXAMPLE?? 
%
%\paragraph{\bf Blood glucose regulation.}
   %\begin{figure}[t]
%\centering
%\includegraphics[width=0.5\textwidth]{glucose.pdf} 
%\caption{Glucose metabolism} \label{fig:glucose}
%\end{figure}
%Here  \emph{glucose regulation} in human body (Figure \ref{fig:glucose}). %as it is a familiar process and it shows that our model is not limited to genetic regulations but it may express other kinds of interactions. 
%We are always referring to the process under normal circumstances in a healthy body.
%
%Glucose regulation is a homeostatic process: \ie the rates of glucose in blood (\emph{glycemia}) must remain stable at what we call the equilibrium state. 
%Glycemia is regulated by  two hormones: \emph{insulin} and  \emph{glucagon}. When glycemia rises (for instance as a result of the digestion of a meal), insulin  promotes the storing of glucose in muscles through the  glycogenesis process, thus decreasing the blood glucose levels. 
%Conversely, when glycemia is critically low, glucagon  stimulates the process of glycogenolysis that increases the blood glucose level by transforming glycogen back into glucose.
%
%
%We will focus on the assimilation of sweeteners: \ie sugars  or  artificial sweeteners such as aspartame. Whenever we eat something sweet either natural or artificial, the sweet sensation sends a signal to the brain (through \emph{neurotransmitters}) that in turns stimulates the production of insulin by pancreas. In the case of sugar, the digestion transforms food into nutrients (\ie glucose) that are absorbed by blood.
%This way, sugar through digestion  increases glucose in blood giving the sensation of satiety. In case the income of glucose produces hyperglycemia,  the levels of glucose are promptly equilibrated by the intervention of insulin.
%Unlike sugar, artificial sweeteners are not assimilated by the body, hence they do not increase the glucose levels in blood. Nevertheless  the insulin produced under the stimuli originated by the sweet sensation can cause the rate of glucose to drop engendering hypoglycemia. In response to that, the brain induces the  stimulus of \emph{hunger}. As a matter of fact this appears as an unwanted/toxic behavior, indeed the assimilation of food (even if it contains aspartame) should calm hunger and induce satiety, and not the opposite. 
%
%This schema suggests that we should consider four  levels for glycemia: low, hunger, equilibrium and high. Likewise for insulin we assume three levels: inactive, low and high. All other actors involved in glucose regulation, have only two  levels (inactive or active).  
%In this example, concerning the durations of activities, all complementary ones such as production of insulin and glucagon,  take the same amount of time, the signal to the brain is the fastest, and the decay of  glycemia values are much longer than the digestion process. We also assume that all activities are potential.  
%Thus the set of entities involved,  their expression levels and the corresponding decays are:
 %$$ \begin{array}{llll}
%\entities = \{&
      %Sugar &\setlev_{sugar}=\{0,1\} & \life_{sugar}(1)=2 \\
  %&    Aspartame \quad &\setlev_{aspartame}=\{0,1\} & \life_{aspartame}(1)=2 \\
%%  & Neurotransmitter \  &\setlev_{NT}=\{0,1\} & \life_{NT}(1)=2 \\
  %& Glycemia &\setlev_{glycemia}=\{0,1,2,3\} \quad & \life_{glycemia}(1)=8 \\
  %&&& \life_{glycemia}(2)=8\\
  %&&& \life_{glycemia}(3)=8\\
  %& Glucagon &\setlev_{glucagon}=\{0,1\} & \life_{glucagon}(1)=3\\
  %&  Insulin &\setlev_{insulin}=\{0,1,2\} & \life_{insulin}(1)=3\\
  %&&& \life_{insulin}(2)=3\\
    %\end{array}
%$$
 %The levels of glycemia are: 0 corresponding to low, 1 to hunger, 2 to equilibrium and 3 to high. Likewise for insulin we have 0 that corresponds to inactive, 1 to low and 2 to high. All the levels for the other entities are 0 for inactive and 1 for active.
%The set of activity $\Reac = \{\alpha_k=(A_k, I_k, R_k) \mid k\in [1..8]\}$ with corresponding response time $\dur{\alpha_k}$ is:
%$$\begin{array}{l|c|c|c|l}
 %\alpha_k & Activators \ R_k & Inhibitors \ I_k & Results \ P_k &  \dur{\alpha_k} \\
%\hline
  %\rho_1 \ & \{(Sugar,1)\} &\emptyset &\{(Insulin,+), (Glycemia,+)\} & 1\\
  %\rho_2 & \{(Aspartame,1)\}& \emptyset &\{(Insulin,+)\} & 1\\
  %\rho_3 & \emptyset &\{(Glycemia,1)\}& \{(Glucagon,+)\} &1\\
 %% (\rho_4) & \{(Glycemia,1)\} &\{(Glycemia,2)\}& \{(NT,+)\} &1\\
 %% (\rho_5) & \{(Glycemia,2)\} &\{(Glycemia,3)\}& \{(NT,-)\} &1\\
  %\rho_4 & \{(Glycemia,3)\}& \emptyset& \{(Insulin,+)\} &1\\
  %\rho_5 & \{(Insulin,2)\} & \emptyset &\{(Glycemia,-)\} &2\\
  %\rho_6 & \{(Insulin,1), &&&\\
           %& (Glycemia,3)\} & \emptyset &\{(Glycemia,-)\} &2\\
  %\rho_7 & \{(Insulin,1)\} & \{ (Glycemia,2)\} &\{(Glycemia,-)\} &2\\
  %\rho_{8} & \{(Glucagon,1)\} &\emptyset &\{(Glycemia,+)\} &2 %\ {\qed}
   %\end{array}
 %$$
%
%
%
%
%
%\begin{figure}[t]
%\centering
%\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]
%
 %\tikzstyle{place}=[rectangle,rounded corners, thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 %\tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 %\tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 %\tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 %fill=black!20,minimum size=4mm]
 %\tikzstyle{every token}=[font=\small]
%
%
%
 %\node [place, label = above: ] at (2,7) (sugar){$Sugar$};
 %\node [place, label = above: ] at (6,7) (asp){$Aspartame$};
 %\node [place, label = right: ] at (2,4) (glucose){$Glycemia$};
%% \node [place, label = right: ] at (5,5) (nt){$Neurotransmitter$};
 %%\node [place, label = left: ] at (0,2) (glycog){$Glycogenesis$};
%% \node [place, label = right: ] at (4,2) (glycol){$Glycogenolysis$};
 %\node [place, label = right: ] at (-2,4) (gluc){$Glucagon$}; 
 %\node [place, label = right: ] at (6,4) (ins){$Insulin$}; 
 %%\node [place, label = above: ] at (-1,5) (hunger){$Hunger$};
%%\node [place, label = below: ] at (6,5) (clock){$Clock$};
%
%\node [transition, label={[red] right:}] at (2,5.5) (tr1) {1}
  %edge [pre]    node[left] {A}    (sugar)
  %edge [ post]    node[above] {+}   (ins)
  %edge [ post]    node[left] {+}   (glucose);
  %
%\node [transition, label={[red] right:}] at (6,5.5) (tr2) {2}
  %edge [pre]    node[left] {A}    (asp)
  %edge [post]    node[left] {+}   (ins);
%
  %
  %\node [transition, label={[red] right:}] at (0,4) (tr3) {3}
  %edge [pre]    node[above] {I}    (glucose)
  %edge [ post]    node[above] {+}   (gluc);
  %
  %
%\node [transition, label={[red] right:}] at (4,4) (tr4) {4}
  %edge [pre]    node[above] {A}    (glucose)
  %edge [post]    node[above] {+}   (ins);
  %
%
%
%
 %\node [transition, label={[red] right:}] at (4,3) (tr5) {5}
   %edge [pre]    node[above] {A}    (ins)
   %edge [post]    node[above] {-}   (glucose);
   %
   %\node [transition, label={[red] right:}] at (4,2) (tr6) {6}
   %edge [pre]    node[above] {A}    (glucose)
   %edge [pre]    node[above] {A}    (ins)
   %edge [post, bend left=30]    node[above] {-}   (glucose);
 %
%
%\node [transition, label={[red] right:}] at (4,1) (tr7) {7}
  %edge [pre, bend left=35]    node[above] {I}    (glucose)
  %edge [pre]    node[right] {A}    (ins)
%
  %edge [post, bend left =60]    node[left] {-}   (glucose);
%
 %
 %\node [transition, label={[red] right:}] at (0,3) (tr8) {8}
  %edge [pre]    node[below] {A}    (gluc)
  %edge [post]    node[below] {+}   (glucose);
%
%\end{tikzpicture}
 %\caption{Simplified \andy network of glucose metabolism. } \label{fig:randyglucose}
%\end{figure}
%
%
%Figure \ref{fig:randyglucose} shows a simplification of the \andy network $(\entities, \emptyset, \Reac)$. It focuses only on the activity schema linking inputs (\ie activators and inhibitors) to results. 
%Each input arc is labeled with either  letter A or letter I denoting whether the input place is an activator or an inhibitor,  respectively. Likewise, each output arc is labeled with a + or a - to denote increase or decrease of result levels.
%For each activity transition $\alpha$, we have omitted the special place $p_{\alpha}$ and all arcs in the opposite direction. The time transition and its adjacent arcs are omitted as well.
%The numbers inside the transition refers to the corresponding activity.
%
%
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Encoding into Timed automata} \label{sec:timedauto}

Since their introduction in \cite{alur:90,alur:91,alur:94} timed automata 
have been widely used to model complex real time systems and to check their 
temporal properties. Since then many variants have been considered depending 
of synchronization policies (synchronous, urgent, broadcast \cite{uppaal}). 

%\paragraph{\bf Timed automata.}

A timed automaton is an annotated directed (and connected) graph, 
with an initial node and provided with a finite set of non-negative real 
variables called \emph{clocks}. 
Nodes (called \emph{locations}) are annotated with \emph{invariants} 
(predicates allowing to enter or stay in a location).
Arcs are annotated with \emph{guards}, 
\emph{communication labels}, and possibly with some clock \emph{resets}. 
Guards are conjunctions of elementary predicates of the form  
$x~\op~c$, where $\op\in\{>,\geq,=,>,\leq\}$ where $x$ is a clock and 
$c$ a (possibly parameterized) positive integer constant.
As usual, the empty conjunction is interpreted as true. 
The set of all guards and invariant predicates will be denoted by $G$. 

%In figures, locations will be represented by round nodes, the initial one having a double boundary. 

\begin{definition}\label{def:ta} A \emph{timed automaton} $\TA$
is a tuple $(L,l^0,X,\Sigma,\arcs,\inv)$, where 
\begin{itemize}
	\item $L$  is a set of locations with $l^0\in L$ the initial one, $X$ is the set of clocks, 
	\item $\Sigma=\Sigma^s\cup\Sigma^u\cup\Sigma^b$ is a set of communication labels, 
	where $\Sigma_s$ are synchronous, $\Sigma_u$ are synchronous and urgent, 
	and $\Sigma_b$ are broadcast ones,
	\item $\arcs \subseteq L \times (G \cup \Sigma \cup R) \times L$ 
is a set of arcs between locations with a guard in $G$, 
a communication label in $\Sigma\cup\{\epsilon\}$, and a set of clock resets in $R=2^X$;
for all $a\in\Sigma^u$, we require the guard to be $\true$; 
  \item $\inv: L \rightarrow G$ assigns invariants to locations. 
\end{itemize}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

It is possible to define a synchronized product of a set of timed automata 
that work and synchronize in parallel. 
The automata are required to have disjoint sets of locations, but
may share clocks and communication labels which are used for synchronization. 
We define three communication policies: 
\begin{itemize}
	\item \emph{synchronous} communications through
		labels $a\in\Sigma^s$ that require all the automata having label $a$  
		to synchronize on $a$; 
	\item \emph{synchronous urgent} communications through 
		labels $u\in\Sigma^u$ that are synchronous as above but \emph{urgent} meaning that
		there will be no delay if transition with label $u$ can be taken;
  \item \emph{broadcast} communications through labels $b!,b?\in\Sigma^b$ meaning that
	a set of automata can synchronize if one is emitting;
	notice that, a process can always emit (e.g., $b!$) 
	and the receivers ($b?$) must synchronize if they can.
\end{itemize}

The synchronous product $\TA_1\parallel \ldots \parallel \TA_n$ 
of timed automata, where for each $j\in[1,\ldots,n]$, 
$\TA_j = (L_j, l^0_j,X_j,\Sigma_j,\arcs_j,\inv_j)$ and all $L_j$ are 
pairwise disjoint sets of locations is
the timed automaton $\TA=(L, l^0,X,\Sigma,\arcs,\inv)$ such that:
\begin{itemize}
\item $L=L_1\times\ldots\times L_n$ and $l^0=(l^0_1,\ldots,l^0_n)$, 
$X=\bigcup_{j=1}^n X_j$, $\Sigma=\bigcup_{j=1}^n \Sigma_j$,
\item $\forall l=(l_1, \ldots, l_n)\in L\colon \inv(l) = \bigwedge_j \inv_j(l_j)$,
\item $\arcs$ is the set of arcs 
$(l_1, \ldots, l_n) \stackrel{g,a,r}{\longrightarrow} (l'_1, \ldots, l'_n)$
such that (where for each $a\in\Sigma^s\cup\Sigma^u, 
S_a=\{j\mid 1\leq j \leq n, a\in \Sigma^s_j\cup\Sigma^u_j\}$):
	for all $1\leq j \leq n$, if $j\not\in S_a$, then $l_j'=l_j$, otherwise
	there exist $g_j$ and $r_j$ such that 
	$l_j \stackrel{g_j,a,r_j}{\longrightarrow} l_j'\in E_j$; $g=\bigwedge_{j\in S_a} g_j$
	and $r=\bigcup_{j\in S_a} r_j$.
\end{itemize}

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is that of the underlying timed automaton $\TA$
(synchronizing on synchronous and broadcast communication labels) as recalled below, 
with the following notations. 
A location is a vector $l = (l_1, \ldots, l_n)$. 
We write $l[l'_j/l_j, j\in S]$ to denote the location $l$ in which the 
$j$th element $l_j$ is replaced by $l'_j$, for all $j$ in some set $S$.
A valuation is a function $\nu$ from the set of clocks to the non-negative reals. 
Let $\mathbb{V}$ be the set of all clock valuations, and $\nu_0(x) = 0$ 
for all $x \in X$.  
We shall denote by $\nu\vDash F$ the fact that the valuation $\nu$ 
satisfies (makes true) the formula $F$.
If $r$ is a clock reset, we shall denote by $\nu[r]$ 
the valuation obtained after applying clock reset $r\subseteq X$ to $\nu$; 
and if $d\in\mathbb{R}_{> 0}$ is a delay, 
$\nu+d$ is the valuation such that, for any clock $x\in X$, 
$(\nu+d)(x)=\nu(x)+d$.

The semantics of a synchronous product $\TA_1\parallel \ldots \parallel \TA_n$
is defined as a timed transition system $(S,s_0,\rightarrow)$,
where $S = (L_1 \times,\ldots\times L_n) \times \mathbb{V}$ is the set of states, 
$s_0 = (l^0, \nu_0)$ is the initial state, and 
$\rightarrow \subseteq S \times S$ is the transition relation defined by:
\begin{itemize}	
	%\item (silent): $(l,\nu) \rightarrow (l',\nu')$ 
	%if there exists $l_i \stackrel{g,~,r}{\longrightarrow} l'_i$, for some $i$, 
	%such that $l'=l[l'_i/l_i]$, $\nu\vDash g$ 
	%and $\nu'=\nu[r]$, 
	\item (sync): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if 
	there exist arc $l \stackrel{g,a,r}{\longrightarrow} l'\in \arcs$ 
	such that $\nu\vDash g$, $\nu'=\nu[r]$,
	for $S_a=\{j\mid 1\leq j\leq n, a\in\Sigma^s_j\}$, 
	$l'=l[l'_j/l_j, j\in S_a]$, 
	and there is no enabled transition with urgent communication label
	from $(\bar{l},\nu)$;
	
	\item (urgent): as (sync) but $a\in\Sigma^u$ and there is no delay
	if transition with urgent communication label can be taken;
	 
	\item (broadcast): $(\bar{l},\nu) \rightarrow (\bar{l'},\nu')$ if
	there exist an output arc $l_j \stackrel{g_j,b!,r_j}{\longrightarrow} l_j'\in \arcs_j$ 
	and a (possibly empty) set of input arcs of the form
	$l_k \stackrel{g_k,b?,r_k}{\longrightarrow} l_k'\in \arcs_k$ such that 
	for all $k\in K=\{k_1,\ldots,k_m\}\subseteq\{l_1,\ldots,l_n\}\setminus\{l_j\}$,
	the size of $K$ is maximal, $\nu\vDash \bigwedge_{k\in K\cup\{j\}} g_k$,
	$l'=l[l'_k/l_k, k\in K\cup\{j\}]$ and $\nu'=\nu[r_k, k\in K\cup\{j\}]$;
	
	\item (timed): $(l,\nu)\rightarrow (l,\nu+d)$ if $\nu+d\vDash \inv(l)$. 
\end{itemize} 
An example of the behavior of timed automata can be found in Appendix \ref{app:ta}.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{\bf Encoding.}
We are now ready to introduce the encoding of the high-level Petri net formalization of $\andy$, to this aim we need to add some notation:

 \begin{newnotation}
Let $\Tag=\{\beta_1,\ldots,\beta_n\}$ be the set of all obligatory activities identifiers from $\Syn$,
ordered alphabetically, \ie $\beta_i<\beta_j$ if $i<j$. 
We denote by 
\[
\Tag^{\circledast}=\{ seq(h) \mid h\in \mathcal{P}(\Tag) \wedge h\neq\emptyset \} \cup \{ \varepsilon\},
\] 
the set of sequences $seq(h)$ obtained by concatenating the identifiers in non-empty subsets $h$ of $\Tag$, where for each $h=\{\beta_{i_1},\ldots,\beta_{i_m}\mid \forall j,k:~ i_j<i_k \}\in \mathcal{P}(\Tag)$, $seq(h)=\beta_{i_1}\cdots \beta_{i_m}$. We assume that if $\Tag^{\circledast}=\{h_1 \dots h_k\}$, then the $h_i$'s are ordered by decreasing length and alphabetically in such a way that $h_1=\beta_1\cdots\beta_{|\Tag|}$ and $h_k = \varepsilon$. 

Moreover, $\beta_i=h[i]$ is the identifier at the $i$-position, and  $h=h_1-h_2$ is  the sequence of identifier in $h_1$ without those in $h_2$.
  %Let $Lab$ be a set of labels, we denote with 
  %$$Lab^{\circledast} = \{x_1 \cdots x_n \mid n \in [1..|Lab|], \forall i,j \in [1..n], x_i \in Lab \wedge x_i < x_j  \} \cup \{ \varepsilon\}$$ 
  %the set of labels obtained by concatenating in alphabetical order ($<$) the labels in $Lab$, using them at most once.  
  %
  %Labels in $Lab^{\circledast} $ can be alphabetically ordered from the longest to $\varepsilon$ thus we denote  $Lab^{\circledast} = \{t_1 \dots t_n \} $ where $t_1$ is the word composed of all labels in $Lab$ and $t_n = \varepsilon$. 
 \end{newnotation}

 The encoding of an $\andy$ Petri net is the synchronized product of a timed automaton for each entity in \entities  together with a set of auxiliary automata that are used to handle potential and obligatory activities.  
 The idea is that the global behavior of an \andy network is divided into its local counterparts represented by entities. Thus for each entity $\gamma$ we build a timed automata $\TA(\gamma, \level{\gamma})$. The automaton has as many locations as the levels in $\gamma$. The locations together with the clocks variables corresponds to the  encoding of the Petri net marking of $\gamma$.
 The marking of place $p_{\rho}$ (for $\rho \in \Syn \cup \Reac$) is encoded by a clock $w_{\rho}$ in the corresponding timed automaton $\TA(\rho)$.
 
 Each transition of the Petri net is encoded by (a series of) timed automata arcs.
 For each transition $t_{\alpha}$ (corresponding to  potential activity  $\alpha$) involving $\gamma$ there is a (synchronous) arcs in the timed automaton $\TA(\gamma, \level{\gamma})$ whose guard describes its role in the activity (activator, inhibitor or result). Moreover the clock $w_{\alpha}$ in   $\TA{\alpha}$ implements the constraints that the activity $\alpha$ cannot be performed more than once in the interval $\dur{\alpha} $:  $w_{\alpha} \geq \dur{\alpha}$. 
 This way, the synchronous product of all automata will reconstruct the full guard of the activity $\alpha$ and  exactly one synchronized transition in the synchronized product of automata corresponds to the firing of transition $t_{\alpha}$. 
 
 Transition $t_c$ is trickier as time progression causes  the simultaneous action of obligatory activities and possibly decay. To this aim, the implementation of $t_c$ has two phases. The first one selects the largest set of enabled obligatory activities and forces the time to progress in a discrete fashion, and the second phase completes the time progression and synchronizes all timed automata.
 Both phases are initiated by   automaton $\TA_{\tick}$ which has two types of arcs: broadcast ones for the first phase and urgent synchronous ones for the second (see Figure \ref{fig:tick}).

\begin{figure}[h!]
\centering
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$l_{\beta_1\beta_2}$}; 
\node[location]  at (2,0) (l2) {$l_{\beta_1}$};
\node[location]  at (4,0) (l3) {$l_{\beta_2}$};
\node[location]  at (6,0) (l4) {$l_{\epsilon}$};
\node[location]  at (8,0) (l5) {$l_{\bot}$};
\draw[->] (l1) -- node[midway,above] {$\beta_1\beta_2!$} (l2) ;
\draw[->] (l2) -- node[midway,above] {$\beta_1!$} (l3) ;
\draw[->] (l3) -- node[midway,above] {$\beta_2!$} (l4) ;
\draw[->] (l4) -- node[midway,above] {$\epsilon!$} (l5) ;
\draw[->, rounded corners] (l2) -- node[midway,right] {$\tick\beta_1\beta_2$}(2,1.5) -- (1,1.5) --  (l1) ;
\draw[->, rounded corners] (l3) -- node[midway,right] {$\tick\beta_1$}(4,2) -- (1,2) --  (l1) ;
\draw[->, rounded corners] (l4) -- node[midway,right] {$\tick\beta_2$}(6,2.5) -- (1,2.5) --  (l1) ;
\draw[->, rounded corners] (l5) -- node[midway,right] {$\tick\epsilon$}(8,3) -- (1,3) --  (l1) ;

\end{tikzpicture}
\caption{The shape of timed automaton $\TA_\tick$ for $\Tag^\circledast=\{\beta_1\beta_2,\beta_1,\beta_2,\epsilon\}$, where $\tick\beta_1\beta_2$, $\tick\beta_1$, $\tick\beta_2$, $\tick\epsilon$ are all synchronous urgent communication labels.}
\label{fig:tick}
\end{figure}


 $\TA_{\tick}$ progressively interrogates the entities timed automata $\TA(\gamma, \level{\gamma})$ and the obligatory activities automata $\TA(\beta_i)$ through broadcast arcs labeled with sequences of obligatory activities identifiers $h\in\Tag^\circledast$, from the longest ($h=seq(\Tag)=\beta_1\cdots\beta_n$) to the shortest ($h=\epsilon$, \ie no obligatory activity is enabled).
 As broadcast is a non blocking transition and because of the ordering on sequences in $\Tag^\circledast$, each entity automaton chooses its maximal set of obligatory activities (plus possible decay) it is involved in. Moreover, when all automata $\TA(\gamma, \level{\gamma})$ and $\TA(\beta_{i})$ have agreed on some sequence $h=\beta_{i_1} \dots \beta_{i_m}$ the first phase is completed and $\{ \beta_{i_1},  \dots,  \beta_{i_m}\}$ is the largest set of enabled obligatory activities. The second phase is then implemented with an urgent synchronous arc synchronizing all automata $\TA_{\tick}$, $\TA(\gamma, \level{\gamma})$, for each $\gamma \in \entities$, and $\TA(\beta_i)$, for $i\in [i_1..i_m]$.
 Notice that guards on broadcast transition constraints the clocks to progress of one time unit at once.   
 As a consequence, timed automata of entities and corresponding clocks evolution exactly encode the marking reached after firing $t_c$.
 
 
 
 
 
 
 
 More formally:
 
 \begin{definition} Given an \andy network $(\entities, \Syn, \Reac)$, with initial expression level $\level{\gamma}$ for each $\gamma \in \entities$, the corresponding timed automata encoding is 
 $$\enc{(\entities, \Syn, \Reac)}= \prod_{\gamma \in \entities} \TA(\gamma,\level{\gamma}) \parallel \prod_{\alpha \in  \Reac} \TA(\alpha) \parallel \prod_{\beta \in \Syn} \TA(\beta) \parallel \TA_{\tick} $$  
 where $\TA(\gamma, \level{\gamma})$, $\TA(\alpha)$,$\TA(\beta)$  and $\TA_{\tick}$ are defined next. In the following we assume $ \Tag = \{\beta \mid \beta \in \Syn \}$ of identifiers of obligatory activities in $\Syn$. \\
 \paragraph{\bf Entities.}
 $\TA(\gamma, \level{\gamma}) = (L_{\gamma},l^0_{\gamma},X_{\gamma},\Sigma_{\gamma}, \arcs_{\gamma} ,\inv_{\gamma})$
  where:
  \begin{itemize}
   \item $L_{\gamma}=\{l^{\gamma}_i \mid i \in [0 ..\setlev_{\gamma} ]\} \cup \{k_i^h,k_i^{d,h} \mid i \in [0 ..\setlev_{\gamma} ], h\in \Tag^{\circledast} \}$ with  $l^0_{\gamma} = l^{\gamma}_{\level{\gamma}}$
   \item $X_{\gamma}=\{\birth^{\gamma}_i, \refr^{\gamma}_i \mid i \in [0 ..\setlev_{\gamma} ]\} \cup \{x_{\gamma}\}$
   \item $\Sigma^s_{\gamma} =  \{  \alpha \mid \alpha \text{ identifier of an activity in }  \Reac  \}$, $  \Sigma_{\gamma}^b =  \Tag^{\circledast}$, $\Sigma_{\gamma}^u =  \{\tick h \mid h \in \Tag^{\circledast} \} $ 
   \item $\arcs_{\gamma} = \arcs_{\Reac} \cup \arcs_{\Syn}$ where 
$$
\arcs_{\Reac} = \{ l_j \xrightarrow{g(A_{\alpha}) \wedge g(I_{\alpha}) \wedge x_{\gamma} = 0, \alpha, r} l_e \mid \gamma_{A_{\alpha}} \leq j < \gamma_{I_{\alpha}}, \alpha \in \Reac, \gamma \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}  
$$
with  $j, e, \gamma_{A_{\alpha}}$, and $\gamma_{I_{\alpha}}$ are levels of $\gamma$ defined as follows:
    
    $$\gamma_{A_{\alpha}} = \begin{cases}
                \level{a} & \text{if } (\gamma, \level{a}) \in {A_{\alpha}}     \\
                0 & \text{otherwise}
               \end{cases}
\qquad 
\gamma_{I_{\alpha}} = \begin{cases}
               \level{i} & \text{if } (\gamma, \level{i}) \in {I_{\alpha}}\\
                \setlev_{\gamma} & \text{otherwise}
               \end{cases}
$$

$$ g(A_{\alpha}) = \begin{cases}
\birth^{\gamma}_{\level{a}} \geq \dur{\alpha} & \text{if } (\gamma, \level{a}) \in A_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
\ 
g(I_{\alpha}) = \begin{cases}
\birth^{\gamma}_{\level{i}} \geq \dur{\alpha} & \text{if } (\gamma, \level{i}) \in I_{\alpha}\\
           \true & \text{otherwise}
          \end{cases}
$$

$$e = \begin{cases}
               \max(0, \min(j+z, \setlev_{\gamma}-1)) & \text{if } (\gamma, z) \in R_{\alpha} \\
                j & \text{otherwise}
               \end{cases}
$$

$$r = \begin{cases}
        \emptyset & \text{if } (\gamma, z) \not \in R_{\alpha}  \\
        \{u^\gamma_e,\} \cup \{\birth_x^{\gamma} \mid x \in [j+1,e]\} & \text{if } (\gamma, z) \in R_{\alpha}  \wedge e-j>0\\
        \{u^\gamma_e,\} & \text{if } (\gamma, z) \in R_{\alpha}  \wedge e-j=0\\
        \{u^\gamma_e,\} \cup \{\birth_x^{\gamma} \mid x \in [e+1,j]\} & \text{if } (\gamma, z) \in R_{\alpha}  \wedge e-j<0
      \end{cases}
$$
$$
\begin{array}{ll}
 \arcs_{\Syn} = & \{ l_j \xrightarrow{g(d)\wedge g , h?, \emptyset} k_j^{d,h},  \mid  j \in [0..\setlev_{\gamma}-1], h\in \Tag^{\circledast}\} \ \cup \\
               & \{ l_j \xrightarrow{\neg g(d)\wedge g , h?, \emptyset} k_j^h,  \mid  j \in [0..\setlev_{\gamma}-1], h\in \Tag^{\circledast}\} \ \cup \\
              & \{ k_j^{d,h} \xrightarrow{\true, h', r \cup \{x_{\gamma}\} } l_e,  \mid  j \in [0..\setlev_{\gamma}-1], h,h' \in \Tag^{\circledast}, h<h' \}\ \cup \\ 
              & \{ k_j^h \xrightarrow{\true, \tick h', r'\cup \{x_{\gamma}\} } l_e',  \mid  j \in [0..\setlev_{\gamma}-1], h,h' \in \Tag^{\circledast}, h<h' \}
\end{array}
$$
where
$$\begin{array}{ll}
   g = & \! \bigwedge_{k=1}^{n} g(\beta_k)  \wedge \bigwedge_{k=1}^{m} \neg g(\beta'_m)\text{ for } h=\beta_1 \cdots \beta_n \text{ and } h_1- h= \beta'_1 \cdots \beta'_m \\
   g(\beta) = & g'(A_\beta) \wedge g'(I_\beta) \text{ and } \beta= \activ{A_\beta}{I_\beta}{\dur{\beta}}{R_\beta}\\
   g(d) = & u_j > \life_{\gamma}(j)
  \end{array}
$$    


$$ g'(A_\beta) = \begin{cases}
j \geq \level{a} \wedge \birth^{\gamma}_{\level{a}} \geq \dur{\beta} & \text{if } (\gamma, \level{a}) \in A_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$
$$
g'(I_\beta) = \begin{cases}
j<\level{i} \wedge \birth^{\gamma}_{\level{i}} \geq \dur{\beta} & \text{if } (\gamma, \level{i}) \in I_\beta\\
           \true & \text{otherwise}
          \end{cases}
$$

$$
\begin{array}{ll}
e = & \max(0, \min(\sum_{i\in[1..n]} f(h[i]') +j -1, \setlev_{\gamma}-1)) \\
e' = & \max(0, \min(\sum_{i\in[1..n]} f(h[i]')+j, \setlev_{\gamma}-1)) \\
\mbox{ where } f(h[i]) = & \begin{cases}
        z & \text{if }  (\gamma, z) \in R_{\beta_i} \\
        0 & \text{otherwise} 
       \end{cases}
\end{array}
$$
$$
\begin{array}{ll}

r = &\begin{cases}
        \{u^\gamma_e\} \cup \{\birth_x^{\gamma} \mid x \in [j+1,e]\} & \text{if }  e-j>0\\
        \{u^\gamma_e\} & \text{if }   e-j=0 \\
        \{u^\gamma_e\} \cup \{\birth_x^{\gamma} \mid x \in [e+1,j]\} & \text{if }   e-j<0     
      \end{cases}
      \\
r' = &\begin{cases}
        \{u^\gamma_{e'}\} \cup \{\birth_x^{\gamma} \mid x \in [j+1,e']\} & \text{if }  e'-j>0\\
        \{u^\gamma_{e'}\} & \text{if }  \gamma \in h'  \wedge e'-j=0 \\
        \{u^\gamma_{e'}\} \cup \{\birth_x^{\gamma} \mid x \in [e'+1,j]\} & \text{if }   e'-j<0 \\
        \emptyset & \text{if }  \gamma \notin h' 
        
      \end{cases}

\end{array}
      $$
where $\gamma \in h$ denotes the formula: $\exists \beta_k=\activ{A_{\beta_k}}{I_{\beta_k}}{\dur{\beta_k}}{R_{\beta_k}}$ s.t. $h=\beta_1\cdots \beta_n, 1\leq k \leq n \wedge (\gamma, z) \in R_{\beta_k}$ 
    
   \item $Inv_{\gamma}(l^{\gamma}_i) = \refr^{\gamma}_i \leq \life_{\gamma}(i)$ for all $i \in [0 ..\setlev_{\gamma}]$
   
  \end{itemize}

  \paragraph{\bf Potential activity.}
$\TA(\alpha) = (L_{\alpha},l^0_{\alpha},X_{\alpha},\Sigma_{\alpha},\arcs_{\alpha},\inv_{\alpha})$  for $\alpha \in \Reac$ where  $L_{\alpha}=\{l_\alpha\}$,  $l^0_{\alpha} = \alpha$, $X_{\alpha}= \{w_{\alpha}\}$,  $\Sigma^s_{\alpha} = \{ \alpha \} $,  $\arcs_{\alpha} = \{ l_\alpha \xrightarrow{w_{\alpha} \geq  \dur{\alpha}, \alpha, \{ w_{\alpha}\}} l_\alpha \}$ and  $\inv_{\alpha}(l_{\alpha}) = \true$.
  
  \paragraph{\bf Obligatory activity.} $\TA(\beta) = (L_{\beta},l^0_{\beta},X_{\beta},\Sigma_{\beta},\arcs_{\beta},\inv_{\beta})$  for $\beta \in \Syn$ where
  \begin{itemize}
   \item $L_{\beta}=\{l_\beta, l'_\beta\}$,  $l^0_{\beta} = l_\beta$,  $X_{\beta}= \{w_{\beta}\}$,  $\Sigma_{\beta}^b =  \Tag^{\circledast}$,  $
\Sigma_{\beta}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\beta} = \{ l_\beta \xrightarrow{w_{\beta} \geq  \dur{\beta}, h?, \emptyset} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \} \cup \{ l'_\beta \xrightarrow{\true, \tick h, \{w_{\beta}\}} l'_\beta \mid h\in \Tag^{\circledast}, \beta\in h \}$
   \item $\inv_{\beta}(l_{\beta}) = \true$ and $\inv_{\beta}(l'_{\beta}) = \true$.
  
  \end{itemize}
  
  \paragraph{\bf Time.}  $\TA_{\tick} = (L_{\tick},l^0_{\tick},X_{\tick},\Sigma_{\tick},\arcs_{\tick},\inv_{\tick})$ where
  \begin{itemize}
   \item $L_{\tick}=\{l_h \mid h \in \Tag^{\circledast}\} \cup \{l_{\bot}\}$,  $l^0_{\tick} = l_{h_1}$,  $X_{\tick}= \{x\}$, $\Sigma_{\tick}^b =  \Tag^{\circledast}$, $ 
\Sigma_{\tick}^u =  \{ \tick h \mid h\in \Tag^{\circledast}\} $
   \item $\arcs_{\tick} =\begin{array}{l}
 \{l_{h_i} \xrightarrow{x=1, h_i!, \emptyset } l_{h_i+1}, l_{h_i+1} \xrightarrow{\true, \tick h_i, \{x\} } l_{h_1} \mid h,  i \in [1..n-1]   \}  \\
\cup \ \{ l_{h_n} \xrightarrow{x=1, h_n!, \emptyset } l_{\bot}, l_{\bot} \xrightarrow{\true, \tick\varepsilon, \{x\} } l_{h_1}   \}
                  \end{array}
$
   \item $\inv_{\tick}(l) = \true$ for all $l \in L_{\tick}$.
  
  \end{itemize}
  
  
  
 \end{definition}

It is easy to see that the following holds:
 
  \begin{theorem}
Given an \andy network $(\entities, \Syn, \Reac)$, %its encoding 
$\enc{(\entities, \Syn, \Reac)}$  is correct and complete.
\end{theorem}
\begin{proof}[sketch]
 Follows by induction on the length of the run and from a case analysis on the transition performed. 
\end{proof}
 
 
\section{Related works and concluding remarks}\label{sec:concl}

This work is inspired by the definition of  
reaction systems \cite{DBLP:journals/ijfcs/BrijderEMR11}, \ie
sets of \emph{reactions}, each of them defined as a triple $(R, I, P)$ with $R$ a set of \emph{reactants}, $I$ the set of \emph{inhibitors} and $P$ the set of \emph{products}, where $R,I$ and $P$ are taken from a common set of \emph{species}. Reaction systems are based on three foundational principles: 
\begin{enumerate}[1.]
 \item \label{item:react} a reaction can take place only if all the reactants involved are available but none of the inhibitors is; 
 \item \label{item:quantity} if a species is available then a sufficient amount of it is present to trigger a reaction; \looseness=-1
 \item species are not persistent: they become unavailable if they are not sustained by a reaction.
\end{enumerate}
From this model we retained the idea of reaction (that we called \emph{activity}) 
but we significantly changed the semantics and domain of application. 
The first change concerns principle \ref{item:quantity}: species here called entities are available at a given discrete   
level, and there is a finite number of levels for each entity.  
The second and more fundamental change concerns the introduction of discrete time constraints. 
Time plays a role in the evolution of entities themselves and in the duration of activities. 
More precisely, entities may have an associated aging function $\delta$, meaning that their  
level diminishes with time.


The main application of our work concerns the verification of properties of systems defined in terms of  rules or activity. 
From a technical point of view, the closest related work is on reaction systems \cite{DBLP:journals/ijfcs/BrijderEMR11} or their Petri net representation \cite{koutnyreaction}. Also, although we use a similar definition for activity, the semantics that we have proposed is inherently different: in \cite{DBLP:journals/ijfcs/BrijderEMR11}  all  enabled reactions occur in one step while we consider an interleaving semantics. 
Moreover, we have introduced discrete abstract  levels that, to the best of our knowledge, are not taken into account in reaction systems.
Also, we have presented a more elaborated notion of time that governs both entities and activity. 
In  \cite{DBLP:conf/birthday/BrijderER11}, the authors consider an extension of reaction systems with duration but it concerns only decay and not  duration of activities. Furthermore the decay is  referred to the number of steps and not to an independent clock. 
In fact, our representation of time is considerably different from the approaches traditionally used in time and timed Petri nets 
(\cite{DBLP:journals/tcs/CeroneM99} presents a survey with insightful comparison of the different approaches).
The main difference lies on the fact that the  progression of time is implicit and  external to the system. By contrast, in our proposal we have assumed the presence of  an explicit way of incrementing time intervals. 
This is also  different from the notion of timestamps introduced in  \cite{timestamp} that again refers to an implicit notion of time.
Indeed,  our approach is closer to Petri nets with causal time  \cite{DBLP:journals/entcs/ThanhKP02} for the presence of explicit clocks and corresponding update transitions but in \andy networks time cannot be suspended under the influence of the environment.
 
In a broader sense, our work could also be related to P-systems \cite{DBLP:journals/ijfcs/PaunPRS11,DBLP:journals/fuin/KleijnK11} or the $\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} that  describe the evolution of cells through rules. 
Both these approaches are mainly oriented to simulation while we are interested in  verification aspects. Finally, always related to the modeling in Petri nets but with a different aim,  levels have been used in qualitative approaches to address problems related to the identification of steady states in genetic networks such as in \cite{DBLP:journals/nc/ChaouiyaNRT11}.  Nevertheless these contributions abstract away from time related aspects that are instead central in our proposal. 

\section{Conclusion and future work}
DISCUSSION ON FUTURE WORKS....

We have introduced \andy, a high-level Petri net framework to model time-dependent systems. In \andy, systems consist of a set of entities present in the environment at a given  level. Entities can age as time passes by and their presence is governed by a  set of rules (activities). In an activity, entities can have the role of activator, inhibitors or results. An activity has a given duration, and it can take place only if all activators are available and all  inhibitors are not for the whole duration of the activity. Depending on the type of activity, results  levels are either increased, maintained or decreased. .  
Moreover, we have illustrated our framework  in the modeling of mobile phone batteries and blood glucose regulation. This highlights  the capability  of \andy to formalize various kinds of domains.



%% 
%Related: reaction systems, petri nets with causal time and petri nets with timestamps
%


\subsubsection*{Acknowledgments.}
This work was supported by the French project ANR BLANC 0307 01 - SYNBIOTIC.
 

\bibliographystyle{abbrv}
\bibliography{biblio}

\appendix
\section{Mobile phone battery}\label{app:mobile}

% \paragraph{\bf..}
% We develop here the example mentioned in the introduction.
% 
%  
%  The set of entity involved:
%  $$ \begin{array}{lll}
%       B &\setlev_{B}=\{5\} & \life_{B}(i)=5, 0<i<5 \\
%       M \ &\setlev_{M}=\{2\} &  \\
%       App &\setlev_{App}=\{3\} \ & \life_{App}(2)=4 
%     \end{array}
% $$
% 
% The set of obligatory activities:
% $$\begin{array}{l|c|c|c|l}
% % \rho_k & A \ A_k & I \ I_k & R \ R_k &  \dur_k \\
% %\hline
%   \rho_1 \ & \{(M,0)\} & \{(M,1)\} &\{(B,+1)\}& 1\\
%   \rho_2 & \{(App,1)\}& \{(App,2)\} & \{(B,-1)\} & 1\\
%   \rho_3 & \{(App,2)\}&  & \{(B,-2)\} & 1
%  \end{array}
%  $$
%  
% The set of potential activities:
% $$\begin{array}{l|c|c|c|l}
%   \rho_4 &  \{(App,0)\}& \emptyset & \{(App,+2)\} & 0\\
%   \rho_5 & \{(M,1)\} & \emptyset &\{(M,-1 )\} &0
%    \end{array}
%  $$

% \begin{figure}[t]

This figure has been generated by the \andy implementation via the Snakes library \cite{} AGGIUNGERE CITAZIONE FRANK POMMERAU!!!
\begin{center}
  \includegraphics[width=\textwidth]{mobile.png}
\end{center}


\section{High level Petri nets - example}\label{app:exfiring}

Here we detail a simple example of firing. Let this be the state of the Petri net before the transition:
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){$7$};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){$5$};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){};
  
  \node [transition] (t) [  label={[red] above:$\begin{array}{c}
                                                x>y ~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}
then by letting $\sigma = \{ x= 7, y=5, x'=12\}$,  after the firing we obtain 
\begin{center}
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

  \node [place, label = left: $p_1$] at (-1.5,0) (Q1){};
  \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){};
  \node [place, label = right: $p_3$] at (1.5,0) (Q3){12};
  
  \node [transition] (t) [  label={[red] above:$\begin{array}{c}
                                                x>y~\wedge \\ x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[below] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[below]{$x'$}    (Q3);
\end{tikzpicture}
\end{center}


% \begin{figure}[t]
% \centering
% \subfigure[Before the firing\label{fig:before}]{
% \begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]
% 
%  \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
%  \tikzstyle{transition}=[rectangle,thick,draw=black!75,
%  			 fill=black!20,minimum size=4mm]
%  \tikzstyle{every token}=[font=\small]
% 
%   \node [place, label = left: $p_1$] at (-1.5,0) (Q1){$7$};
%   \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){$5$};
%   \node [place, label = right: $p_3$] at (1.5,0) (Q3){};
%   
%   \node [transition] (t) [  label={[red] above:$\begin{array}{c}
%                                                 x>y ~\wedge \\ x'=x+y
%                                                \end{array}$}] at (0,0) {$t$}
%    edge [pre]    node[below] {$x$}    (Q1)
%    edge [pre]    node[right] {$y$}    (Q2)
%    edge [post]   node[below]{$x'$}    (Q3);
% \end{tikzpicture}} \quad
% \subfigure[After the firing \label{fig:after}]{
% \begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]
% 
%  \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
%  \tikzstyle{transition}=[rectangle,thick,draw=black!75,
%  			 fill=black!20,minimum size=4mm]
%  \tikzstyle{every token}=[font=\small]
% 
%   \node [place, label = left: $p_1$] at (-1.5,0) (Q1){};
%   \node [place, label=left:$p_2$]at (0,-1.5)  (Q2){};
%   \node [place, label = right: $p_3$] at (1.5,0) (Q3){12};
%   
%   \node [transition] (t) [  label={[red] above:$\begin{array}{c}
%                                                 x>y~\wedge \\ x'=x+y
%                                                \end{array}$}] at (0,0) {$t$}
%    edge [pre]    node[below] {$x$}    (Q1)
%    edge [pre]    node[right] {$y$}    (Q2)
%    edge [post]   node[below]{$x'$}    (Q3);
% \end{tikzpicture}}
% \caption{Example of firing with $\sigma = \{ x= 7, y=5, x'=12\}$.} \label{fig:exfiring}
% \end{figure}

% \caption{High level Petri net generated via the Snakes library} %\label{fig:mobile}
% \end{figure}

\section{Timed automata - example}\label{app:ta}
%\begin{figure}[htbp]
%\centering
%\subfigure[$\TA_1\parallel \TA_2$]{
Here we exemplify timed automata usage: 
Consider for instance the network of timed automata $\TA_1$ and $\TA_2$:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.8, yscale=.6,every node/.style={scale=0.7}]
\node[location,double] at (0,0) (l1) {$\stackrel{l_1}{x < 2}$}; 
\node[location]  at (4,0) (l2) {$\stackrel{l_2}{x < 2}$};
\node[left] at (-4,0) {$\TA_1$};
\node[location,double] at (0,-2) (l3) {$\stackrel{l_3}{\emptyset}$};
\node[location] at (4,-2) (l4) {$\stackrel{l_4}{\emptyset}$};
\draw[->, rounded corners] (l2) -- (5,-.5) -- (5.5,-.5) -- node[midway,right] 
				{$x>0;b;\emptyset$}  (5.5,.5) -- (5,.5)-- (l2) ;

\node[left] at (-4,-2) {$\TA_2$};
\draw[->] (l1) -- (l2) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l3) -- (l4) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l3) -- (-1,-2.5) -- (-1.5,-2.5) -- node[midway,left] 
				{$\true;a;\{x\}$}  (-1.5,-1.5) -- (-1,-1.5)-- (l3) ;
\end{tikzpicture}
\end{center}
%}
%%%
%\subfigure[$sync(\TA_1\parallel \TA_2)$]{
whose behavior is given by their synchronized product $\TA_1\parallel \TA_2$:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=.9, yscale=.6,every node/.style={scale=0.7}]
\node[location]  at (0,0) (l14) {$\stackrel{(l_1,l_4)}{x < 2}$};
\node[location,double] at (3,0) (l13) {$\stackrel{(l_1,l_3)}{x < 2}$}; 
\node[location] at (6,0) (l23) {$\stackrel{(l_2,l_3)}{x < 2}$};
\node[location] at (9,0) (l24) {$\stackrel{(l_2,l_4)}{x < 2}$};
\draw[->, rounded corners] (l23) -- (5.5,1) -- (5.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (6.5,1.5) -- (6.5,1)-- (l23) ;
\draw[->] (l13) -- (l14) node[midway,above] {$x=1;c;\emptyset$};
\draw[->] (l13) -- (l23) node[midway,above] {$x=1;a;\{x\}$};
\draw[->] (l23) -- (l24) node[midway,above] {$x=1;c;\emptyset$};
\draw[->, rounded corners] (l24) -- (8.5,1) -- (8.5,1.5) -- node[midway,above] 
				{$x>0;b;\emptyset$}  (9.5,1.5) -- (9.5,1)-- (l24) ;
\end{tikzpicture}
\end{center}
%}
%%%
%HK doit être modifié pour inclure des canaux broadcast
%\subfigure[A possible run]{
and where a possible run is:
\begin{center}
\begin{tikzpicture}[>=latex',xscale=1, yscale=.6,every node/.style={scale=0.7}]
\node at (0,0) (e1) {$[(l_1,l_3);x=0]$}; // t+1
\node at (2,0) (e2) {$[(l_1,l_3);x=1]$}; // a
\node at (4,0) (e3) {$[(l_2,l_3);x=0]$}; // t+.5
\node at (6,0) (e4) {$[(l_2,l_3);x=.5]$}; // b
\node at (8,0) (e5) {$[(l_2,l_3);x=.5]$}; // t+.5
\node at (10,0) (e6) {$[(l_2,l_4);x=1]$}; 
\draw[->] (e1) -- (e2) ;
\draw[->] (e2) -- (e3) ;
\draw[->] (e3) -- (e4) ;
\draw[->] (e4) -- (e5) ;
\draw[->] (e5) -- (e6) ;
\end{tikzpicture}
\end{center}
%}
%\caption{A network of timed automata with a possible run.}
%\label{fig:ta}
%\end{figure}



\end{document}
